Nuprl Lemma : zero_ann_b
13,42
postcript
pdf
a
,
b
:
. (
((
a
*
b
) = 0))
((
(
a
= 0)) & (
(
b
= 0)))
latex
Up
int
2
,
int
2
Definitions
,
t
T
,
P
&
Q
,
A
,
P
Q
,
x
:
A
.
B
(
x
)
,
False
Lemmas
not
wf
origin
a, b:
. (
((a * b) = 0)) 
(((a = 0)) & ((b = 0))) a, b:. (((a * b) = 0)) (((a = 0)) & ((b = 0))) 
TA Qx:A. B(x)